greatcfandomcom-20200214-history
Lambda Calculus
The Language Abstract Syntax A Recursive Definition Lambda expressions are composed of * variables x, y, z, ... * the symbols \lambda and . The set of lambda expressions, \Lambda , can be defined recursively: # x is a variable, x \in \Lambda # If x is a variable and M \in \Lambda , then \lambda x . M \in \Lambda # If M, \; N \in \Lambda then M \; N \in \Lambda A BNF Definition ::= | "λ" "." | ::= "x" | "y" | "z" | . . . A More Concrete Syntax To enable us to write lambda expressions as strings we introduce brackets. These can be put anywhere. ::= | λ . | | "(" ")" Examples x x y y x x (y y) \lambda x . x \; x \lambda x \; y . \; x \lambda x \; y \; z . (x \; z (y \; z)) Precedence \lambda x . E F = (\lambda x . E F) E \; F \; G = (E \; F) \; G beta Reduction (\lambda x . E ) \; F \rightarrow \beta \rightarrow E / x Free Variables FV(x) = \{ x \} FV(E \; F) = FV(E) \cup FV(F) FV(\lambda x . E) = FV(E) \setminus {x} Some examples: * FV(\lambda x . x) = \emptyset * FV( x \; \lambda x . x) = \{ x \} * FV(x \; y \; z) = \{ x , y , z\} * FV(\lambda y . x \; y \; z) = \{ x , z\} * FV(\lambda y . \lambda z . \lambda x . x \; y \; z) = \emptyset Substitution * x / x = F * y / x = y \; , y \ne x * (G \; H) / x = G / x \; H / x * (\lambda y. G)/ x = \lambda y . G/ x , y \ne x \; and \; y \notin FV(F) * (\lambda y. G)/ x = \lambda z . G/ x/ x , y \ne x \; and \; y \in FV(F) , where \; z \ne y \; and \; z \notin FV(F \; G) Combinators * I = \lambda x . x * S = \lambda x . \lambda y . \lambda z . ( x z ( y z ) ) * K = \lambda x . \lambda y . x Natural Numbers Definition - Church numerals Church numerals \mathbf{0} , \mathbf{1} , \mathbf{2} , ..., are defined as follows in the lambda calculus: : \mathbf{0} \equiv \lambda f.\lambda x. x : \mathbf{1} \equiv \lambda f.\lambda x.f x : \mathbf{2} \equiv \lambda f.\lambda x.f (f x) : \mathbf{3} \equiv \lambda f.\lambda x.f (f (f x)) : ... : \mathbf{n} \equiv \lambda f.\lambda x.f^n x : ... That is, the natural number n is represented by the Church numeral n''', which has the property that for any lambda-terms F and X, : '''n F X =β F''n'' X Haskell * http://www.haskell.org/ Lambda Expression in Haskell: \x -> x x Category:Education